(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
intersect'ii'in(cons(X, X0), cons(X, X1)) → intersect'ii'out
intersect'ii'in(Xs, cons(X0, Ys)) → u'1'1(intersect'ii'in(Xs, Ys))
u'1'1(intersect'ii'out) → intersect'ii'out
intersect'ii'in(cons(X0, Xs), Ys) → u'2'1(intersect'ii'in(Xs, Ys))
u'2'1(intersect'ii'out) → intersect'ii'out
reduce'ii'in(sequent(cons(if(A, B), Fs), Gs), NF) → u'3'1(reduce'ii'in(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF))
u'3'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(iff(A, B), Fs), Gs), NF) → u'4'1(reduce'ii'in(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF))
u'4'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) → u'5'1(reduce'ii'in(sequent(cons(F1, cons(F2, Fs)), Gs), NF))
u'5'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) → u'6'1(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
u'6'1(reduce'ii'out, F2, Fs, Gs, NF) → u'6'2(reduce'ii'in(sequent(cons(F2, Fs), Gs), NF))
u'6'2(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(x'2d(F1), Fs), Gs), NF) → u'7'1(reduce'ii'in(sequent(Fs, cons(F1, Gs)), NF))
u'7'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(if(A, B), Gs)), NF) → u'8'1(reduce'ii'in(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF))
u'8'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(iff(A, B), Gs)), NF) → u'9'1(reduce'ii'in(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF))
u'9'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) → u'10'1(reduce'ii'in(sequent(Fs, Gs), sequent(cons(p(V), Left), Right)))
u'10'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) → u'11'1(reduce'ii'in(sequent(Fs, cons(G1, cons(G2, Gs))), NF))
u'11'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) → u'12'1(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF)
u'12'1(reduce'ii'out, Fs, G2, Gs, NF) → u'12'2(reduce'ii'in(sequent(Fs, cons(G2, Gs)), NF))
u'12'2(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(x'2d(G1), Gs)), NF) → u'13'1(reduce'ii'in(sequent(cons(G1, Fs), Gs), NF))
u'13'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(nil, cons(p(V), Gs)), sequent(Left, Right)) → u'14'1(reduce'ii'in(sequent(nil, Gs), sequent(Left, cons(p(V), Right))))
u'14'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(nil, nil), sequent(F1, F2)) → u'15'1(intersect'ii'in(F1, F2))
u'15'1(intersect'ii'out) → reduce'ii'out
tautology'i'in(F) → u'16'1(reduce'ii'in(sequent(nil, cons(F, nil)), sequent(nil, nil)))
u'16'1(reduce'ii'out) → tautology'i'out
Rewrite Strategy: FULL
(1) DecreasingLoopProof (EQUIVALENT transformation)
The following loop(s) give(s) rise to the lower bound Ω(n1):
The rewrite sequence
intersect'ii'in(Xs, cons(X0, Ys)) →+ u'1'1(intersect'ii'in(Xs, Ys))
gives rise to a decreasing loop by considering the right hand sides subterm at position [0].
The pumping substitution is [Ys / cons(X0, Ys)].
The result substitution is [ ].
(2) BOUNDS(n^1, INF)
(3) RenamingProof (EQUIVALENT transformation)
Renamed function symbols to avoid clashes with predefined symbol.
(4) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:
intersect'ii'in(cons(X, X0), cons(X, X1)) → intersect'ii'out
intersect'ii'in(Xs, cons(X0, Ys)) → u'1'1(intersect'ii'in(Xs, Ys))
u'1'1(intersect'ii'out) → intersect'ii'out
intersect'ii'in(cons(X0, Xs), Ys) → u'2'1(intersect'ii'in(Xs, Ys))
u'2'1(intersect'ii'out) → intersect'ii'out
reduce'ii'in(sequent(cons(if(A, B), Fs), Gs), NF) → u'3'1(reduce'ii'in(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF))
u'3'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(iff(A, B), Fs), Gs), NF) → u'4'1(reduce'ii'in(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF))
u'4'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) → u'5'1(reduce'ii'in(sequent(cons(F1, cons(F2, Fs)), Gs), NF))
u'5'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) → u'6'1(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
u'6'1(reduce'ii'out, F2, Fs, Gs, NF) → u'6'2(reduce'ii'in(sequent(cons(F2, Fs), Gs), NF))
u'6'2(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(x'2d(F1), Fs), Gs), NF) → u'7'1(reduce'ii'in(sequent(Fs, cons(F1, Gs)), NF))
u'7'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(if(A, B), Gs)), NF) → u'8'1(reduce'ii'in(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF))
u'8'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(iff(A, B), Gs)), NF) → u'9'1(reduce'ii'in(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF))
u'9'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) → u'10'1(reduce'ii'in(sequent(Fs, Gs), sequent(cons(p(V), Left), Right)))
u'10'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) → u'11'1(reduce'ii'in(sequent(Fs, cons(G1, cons(G2, Gs))), NF))
u'11'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) → u'12'1(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF)
u'12'1(reduce'ii'out, Fs, G2, Gs, NF) → u'12'2(reduce'ii'in(sequent(Fs, cons(G2, Gs)), NF))
u'12'2(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(x'2d(G1), Gs)), NF) → u'13'1(reduce'ii'in(sequent(cons(G1, Fs), Gs), NF))
u'13'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(nil, cons(p(V), Gs)), sequent(Left, Right)) → u'14'1(reduce'ii'in(sequent(nil, Gs), sequent(Left, cons(p(V), Right))))
u'14'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(nil, nil), sequent(F1, F2)) → u'15'1(intersect'ii'in(F1, F2))
u'15'1(intersect'ii'out) → reduce'ii'out
tautology'i'in(F) → u'16'1(reduce'ii'in(sequent(nil, cons(F, nil)), sequent(nil, nil)))
u'16'1(reduce'ii'out) → tautology'i'out
S is empty.
Rewrite Strategy: FULL
(5) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)
Infered types.
(6) Obligation:
TRS:
Rules:
intersect'ii'in(cons(X, X0), cons(X, X1)) → intersect'ii'out
intersect'ii'in(Xs, cons(X0, Ys)) → u'1'1(intersect'ii'in(Xs, Ys))
u'1'1(intersect'ii'out) → intersect'ii'out
intersect'ii'in(cons(X0, Xs), Ys) → u'2'1(intersect'ii'in(Xs, Ys))
u'2'1(intersect'ii'out) → intersect'ii'out
reduce'ii'in(sequent(cons(if(A, B), Fs), Gs), NF) → u'3'1(reduce'ii'in(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF))
u'3'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(iff(A, B), Fs), Gs), NF) → u'4'1(reduce'ii'in(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF))
u'4'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) → u'5'1(reduce'ii'in(sequent(cons(F1, cons(F2, Fs)), Gs), NF))
u'5'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) → u'6'1(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
u'6'1(reduce'ii'out, F2, Fs, Gs, NF) → u'6'2(reduce'ii'in(sequent(cons(F2, Fs), Gs), NF))
u'6'2(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(x'2d(F1), Fs), Gs), NF) → u'7'1(reduce'ii'in(sequent(Fs, cons(F1, Gs)), NF))
u'7'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(if(A, B), Gs)), NF) → u'8'1(reduce'ii'in(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF))
u'8'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(iff(A, B), Gs)), NF) → u'9'1(reduce'ii'in(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF))
u'9'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) → u'10'1(reduce'ii'in(sequent(Fs, Gs), sequent(cons(p(V), Left), Right)))
u'10'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) → u'11'1(reduce'ii'in(sequent(Fs, cons(G1, cons(G2, Gs))), NF))
u'11'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) → u'12'1(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF)
u'12'1(reduce'ii'out, Fs, G2, Gs, NF) → u'12'2(reduce'ii'in(sequent(Fs, cons(G2, Gs)), NF))
u'12'2(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(x'2d(G1), Gs)), NF) → u'13'1(reduce'ii'in(sequent(cons(G1, Fs), Gs), NF))
u'13'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(nil, cons(p(V), Gs)), sequent(Left, Right)) → u'14'1(reduce'ii'in(sequent(nil, Gs), sequent(Left, cons(p(V), Right))))
u'14'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(nil, nil), sequent(F1, F2)) → u'15'1(intersect'ii'in(F1, F2))
u'15'1(intersect'ii'out) → reduce'ii'out
tautology'i'in(F) → u'16'1(reduce'ii'in(sequent(nil, cons(F, nil)), sequent(nil, nil)))
u'16'1(reduce'ii'out) → tautology'i'out
Types:
intersect'ii'in :: cons:nil → cons:nil → intersect'ii'out
cons :: if:x'2d:x'2b:iff:x'2a:p → cons:nil → cons:nil
intersect'ii'out :: intersect'ii'out
u'1'1 :: intersect'ii'out → intersect'ii'out
u'2'1 :: intersect'ii'out → intersect'ii'out
reduce'ii'in :: sequent → sequent → reduce'ii'out
sequent :: cons:nil → cons:nil → sequent
if :: if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p
u'3'1 :: reduce'ii'out → reduce'ii'out
x'2b :: if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p
x'2d :: if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p
reduce'ii'out :: reduce'ii'out
iff :: if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p
u'4'1 :: reduce'ii'out → reduce'ii'out
x'2a :: if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p
u'5'1 :: reduce'ii'out → reduce'ii'out
u'6'1 :: reduce'ii'out → if:x'2d:x'2b:iff:x'2a:p → cons:nil → cons:nil → sequent → reduce'ii'out
u'6'2 :: reduce'ii'out → reduce'ii'out
u'7'1 :: reduce'ii'out → reduce'ii'out
u'8'1 :: reduce'ii'out → reduce'ii'out
u'9'1 :: reduce'ii'out → reduce'ii'out
p :: a → if:x'2d:x'2b:iff:x'2a:p
u'10'1 :: reduce'ii'out → reduce'ii'out
u'11'1 :: reduce'ii'out → reduce'ii'out
u'12'1 :: reduce'ii'out → cons:nil → if:x'2d:x'2b:iff:x'2a:p → cons:nil → sequent → reduce'ii'out
u'12'2 :: reduce'ii'out → reduce'ii'out
u'13'1 :: reduce'ii'out → reduce'ii'out
nil :: cons:nil
u'14'1 :: reduce'ii'out → reduce'ii'out
u'15'1 :: intersect'ii'out → reduce'ii'out
tautology'i'in :: if:x'2d:x'2b:iff:x'2a:p → tautology'i'out
u'16'1 :: reduce'ii'out → tautology'i'out
tautology'i'out :: tautology'i'out
hole_intersect'ii'out1_3 :: intersect'ii'out
hole_cons:nil2_3 :: cons:nil
hole_if:x'2d:x'2b:iff:x'2a:p3_3 :: if:x'2d:x'2b:iff:x'2a:p
hole_reduce'ii'out4_3 :: reduce'ii'out
hole_sequent5_3 :: sequent
hole_a6_3 :: a
hole_tautology'i'out7_3 :: tautology'i'out
gen_cons:nil8_3 :: Nat → cons:nil
gen_if:x'2d:x'2b:iff:x'2a:p9_3 :: Nat → if:x'2d:x'2b:iff:x'2a:p
(7) OrderProof (LOWER BOUND(ID) transformation)
Heuristically decided to analyse the following defined symbols:
intersect'ii'in,
reduce'ii'inThey will be analysed ascendingly in the following order:
intersect'ii'in < reduce'ii'in
(8) Obligation:
TRS:
Rules:
intersect'ii'in(
cons(
X,
X0),
cons(
X,
X1)) →
intersect'ii'outintersect'ii'in(
Xs,
cons(
X0,
Ys)) →
u'1'1(
intersect'ii'in(
Xs,
Ys))
u'1'1(
intersect'ii'out) →
intersect'ii'outintersect'ii'in(
cons(
X0,
Xs),
Ys) →
u'2'1(
intersect'ii'in(
Xs,
Ys))
u'2'1(
intersect'ii'out) →
intersect'ii'outreduce'ii'in(
sequent(
cons(
if(
A,
B),
Fs),
Gs),
NF) →
u'3'1(
reduce'ii'in(
sequent(
cons(
x'2b(
x'2d(
B),
A),
Fs),
Gs),
NF))
u'3'1(
reduce'ii'out) →
reduce'ii'outreduce'ii'in(
sequent(
cons(
iff(
A,
B),
Fs),
Gs),
NF) →
u'4'1(
reduce'ii'in(
sequent(
cons(
x'2a(
if(
A,
B),
if(
B,
A)),
Fs),
Gs),
NF))
u'4'1(
reduce'ii'out) →
reduce'ii'outreduce'ii'in(
sequent(
cons(
x'2a(
F1,
F2),
Fs),
Gs),
NF) →
u'5'1(
reduce'ii'in(
sequent(
cons(
F1,
cons(
F2,
Fs)),
Gs),
NF))
u'5'1(
reduce'ii'out) →
reduce'ii'outreduce'ii'in(
sequent(
cons(
x'2b(
F1,
F2),
Fs),
Gs),
NF) →
u'6'1(
reduce'ii'in(
sequent(
cons(
F1,
Fs),
Gs),
NF),
F2,
Fs,
Gs,
NF)
u'6'1(
reduce'ii'out,
F2,
Fs,
Gs,
NF) →
u'6'2(
reduce'ii'in(
sequent(
cons(
F2,
Fs),
Gs),
NF))
u'6'2(
reduce'ii'out) →
reduce'ii'outreduce'ii'in(
sequent(
cons(
x'2d(
F1),
Fs),
Gs),
NF) →
u'7'1(
reduce'ii'in(
sequent(
Fs,
cons(
F1,
Gs)),
NF))
u'7'1(
reduce'ii'out) →
reduce'ii'outreduce'ii'in(
sequent(
Fs,
cons(
if(
A,
B),
Gs)),
NF) →
u'8'1(
reduce'ii'in(
sequent(
Fs,
cons(
x'2b(
x'2d(
B),
A),
Gs)),
NF))
u'8'1(
reduce'ii'out) →
reduce'ii'outreduce'ii'in(
sequent(
Fs,
cons(
iff(
A,
B),
Gs)),
NF) →
u'9'1(
reduce'ii'in(
sequent(
Fs,
cons(
x'2a(
if(
A,
B),
if(
B,
A)),
Gs)),
NF))
u'9'1(
reduce'ii'out) →
reduce'ii'outreduce'ii'in(
sequent(
cons(
p(
V),
Fs),
Gs),
sequent(
Left,
Right)) →
u'10'1(
reduce'ii'in(
sequent(
Fs,
Gs),
sequent(
cons(
p(
V),
Left),
Right)))
u'10'1(
reduce'ii'out) →
reduce'ii'outreduce'ii'in(
sequent(
Fs,
cons(
x'2b(
G1,
G2),
Gs)),
NF) →
u'11'1(
reduce'ii'in(
sequent(
Fs,
cons(
G1,
cons(
G2,
Gs))),
NF))
u'11'1(
reduce'ii'out) →
reduce'ii'outreduce'ii'in(
sequent(
Fs,
cons(
x'2a(
G1,
G2),
Gs)),
NF) →
u'12'1(
reduce'ii'in(
sequent(
Fs,
cons(
G1,
Gs)),
NF),
Fs,
G2,
Gs,
NF)
u'12'1(
reduce'ii'out,
Fs,
G2,
Gs,
NF) →
u'12'2(
reduce'ii'in(
sequent(
Fs,
cons(
G2,
Gs)),
NF))
u'12'2(
reduce'ii'out) →
reduce'ii'outreduce'ii'in(
sequent(
Fs,
cons(
x'2d(
G1),
Gs)),
NF) →
u'13'1(
reduce'ii'in(
sequent(
cons(
G1,
Fs),
Gs),
NF))
u'13'1(
reduce'ii'out) →
reduce'ii'outreduce'ii'in(
sequent(
nil,
cons(
p(
V),
Gs)),
sequent(
Left,
Right)) →
u'14'1(
reduce'ii'in(
sequent(
nil,
Gs),
sequent(
Left,
cons(
p(
V),
Right))))
u'14'1(
reduce'ii'out) →
reduce'ii'outreduce'ii'in(
sequent(
nil,
nil),
sequent(
F1,
F2)) →
u'15'1(
intersect'ii'in(
F1,
F2))
u'15'1(
intersect'ii'out) →
reduce'ii'outtautology'i'in(
F) →
u'16'1(
reduce'ii'in(
sequent(
nil,
cons(
F,
nil)),
sequent(
nil,
nil)))
u'16'1(
reduce'ii'out) →
tautology'i'outTypes:
intersect'ii'in :: cons:nil → cons:nil → intersect'ii'out
cons :: if:x'2d:x'2b:iff:x'2a:p → cons:nil → cons:nil
intersect'ii'out :: intersect'ii'out
u'1'1 :: intersect'ii'out → intersect'ii'out
u'2'1 :: intersect'ii'out → intersect'ii'out
reduce'ii'in :: sequent → sequent → reduce'ii'out
sequent :: cons:nil → cons:nil → sequent
if :: if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p
u'3'1 :: reduce'ii'out → reduce'ii'out
x'2b :: if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p
x'2d :: if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p
reduce'ii'out :: reduce'ii'out
iff :: if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p
u'4'1 :: reduce'ii'out → reduce'ii'out
x'2a :: if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p
u'5'1 :: reduce'ii'out → reduce'ii'out
u'6'1 :: reduce'ii'out → if:x'2d:x'2b:iff:x'2a:p → cons:nil → cons:nil → sequent → reduce'ii'out
u'6'2 :: reduce'ii'out → reduce'ii'out
u'7'1 :: reduce'ii'out → reduce'ii'out
u'8'1 :: reduce'ii'out → reduce'ii'out
u'9'1 :: reduce'ii'out → reduce'ii'out
p :: a → if:x'2d:x'2b:iff:x'2a:p
u'10'1 :: reduce'ii'out → reduce'ii'out
u'11'1 :: reduce'ii'out → reduce'ii'out
u'12'1 :: reduce'ii'out → cons:nil → if:x'2d:x'2b:iff:x'2a:p → cons:nil → sequent → reduce'ii'out
u'12'2 :: reduce'ii'out → reduce'ii'out
u'13'1 :: reduce'ii'out → reduce'ii'out
nil :: cons:nil
u'14'1 :: reduce'ii'out → reduce'ii'out
u'15'1 :: intersect'ii'out → reduce'ii'out
tautology'i'in :: if:x'2d:x'2b:iff:x'2a:p → tautology'i'out
u'16'1 :: reduce'ii'out → tautology'i'out
tautology'i'out :: tautology'i'out
hole_intersect'ii'out1_3 :: intersect'ii'out
hole_cons:nil2_3 :: cons:nil
hole_if:x'2d:x'2b:iff:x'2a:p3_3 :: if:x'2d:x'2b:iff:x'2a:p
hole_reduce'ii'out4_3 :: reduce'ii'out
hole_sequent5_3 :: sequent
hole_a6_3 :: a
hole_tautology'i'out7_3 :: tautology'i'out
gen_cons:nil8_3 :: Nat → cons:nil
gen_if:x'2d:x'2b:iff:x'2a:p9_3 :: Nat → if:x'2d:x'2b:iff:x'2a:p
Generator Equations:
gen_cons:nil8_3(0) ⇔ nil
gen_cons:nil8_3(+(x, 1)) ⇔ cons(p(hole_a6_3), gen_cons:nil8_3(x))
gen_if:x'2d:x'2b:iff:x'2a:p9_3(0) ⇔ p(hole_a6_3)
gen_if:x'2d:x'2b:iff:x'2a:p9_3(+(x, 1)) ⇔ if(p(hole_a6_3), gen_if:x'2d:x'2b:iff:x'2a:p9_3(x))
The following defined symbols remain to be analysed:
intersect'ii'in, reduce'ii'in
They will be analysed ascendingly in the following order:
intersect'ii'in < reduce'ii'in
(9) RewriteLemmaProof (LOWER BOUND(ID) transformation)
Proved the following rewrite lemma:
intersect'ii'in(
gen_cons:nil8_3(
a),
gen_cons:nil8_3(
+(
1,
n11_3))) →
*10_3, rt ∈ Ω(n11
3)
Induction Base:
intersect'ii'in(gen_cons:nil8_3(a), gen_cons:nil8_3(+(1, 0)))
Induction Step:
intersect'ii'in(gen_cons:nil8_3(a), gen_cons:nil8_3(+(1, +(n11_3, 1)))) →RΩ(1)
u'1'1(intersect'ii'in(gen_cons:nil8_3(a), gen_cons:nil8_3(+(1, n11_3)))) →IH
u'1'1(*10_3)
We have rt ∈ Ω(n1) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
(10) Complex Obligation (BEST)
(11) Obligation:
TRS:
Rules:
intersect'ii'in(
cons(
X,
X0),
cons(
X,
X1)) →
intersect'ii'outintersect'ii'in(
Xs,
cons(
X0,
Ys)) →
u'1'1(
intersect'ii'in(
Xs,
Ys))
u'1'1(
intersect'ii'out) →
intersect'ii'outintersect'ii'in(
cons(
X0,
Xs),
Ys) →
u'2'1(
intersect'ii'in(
Xs,
Ys))
u'2'1(
intersect'ii'out) →
intersect'ii'outreduce'ii'in(
sequent(
cons(
if(
A,
B),
Fs),
Gs),
NF) →
u'3'1(
reduce'ii'in(
sequent(
cons(
x'2b(
x'2d(
B),
A),
Fs),
Gs),
NF))
u'3'1(
reduce'ii'out) →
reduce'ii'outreduce'ii'in(
sequent(
cons(
iff(
A,
B),
Fs),
Gs),
NF) →
u'4'1(
reduce'ii'in(
sequent(
cons(
x'2a(
if(
A,
B),
if(
B,
A)),
Fs),
Gs),
NF))
u'4'1(
reduce'ii'out) →
reduce'ii'outreduce'ii'in(
sequent(
cons(
x'2a(
F1,
F2),
Fs),
Gs),
NF) →
u'5'1(
reduce'ii'in(
sequent(
cons(
F1,
cons(
F2,
Fs)),
Gs),
NF))
u'5'1(
reduce'ii'out) →
reduce'ii'outreduce'ii'in(
sequent(
cons(
x'2b(
F1,
F2),
Fs),
Gs),
NF) →
u'6'1(
reduce'ii'in(
sequent(
cons(
F1,
Fs),
Gs),
NF),
F2,
Fs,
Gs,
NF)
u'6'1(
reduce'ii'out,
F2,
Fs,
Gs,
NF) →
u'6'2(
reduce'ii'in(
sequent(
cons(
F2,
Fs),
Gs),
NF))
u'6'2(
reduce'ii'out) →
reduce'ii'outreduce'ii'in(
sequent(
cons(
x'2d(
F1),
Fs),
Gs),
NF) →
u'7'1(
reduce'ii'in(
sequent(
Fs,
cons(
F1,
Gs)),
NF))
u'7'1(
reduce'ii'out) →
reduce'ii'outreduce'ii'in(
sequent(
Fs,
cons(
if(
A,
B),
Gs)),
NF) →
u'8'1(
reduce'ii'in(
sequent(
Fs,
cons(
x'2b(
x'2d(
B),
A),
Gs)),
NF))
u'8'1(
reduce'ii'out) →
reduce'ii'outreduce'ii'in(
sequent(
Fs,
cons(
iff(
A,
B),
Gs)),
NF) →
u'9'1(
reduce'ii'in(
sequent(
Fs,
cons(
x'2a(
if(
A,
B),
if(
B,
A)),
Gs)),
NF))
u'9'1(
reduce'ii'out) →
reduce'ii'outreduce'ii'in(
sequent(
cons(
p(
V),
Fs),
Gs),
sequent(
Left,
Right)) →
u'10'1(
reduce'ii'in(
sequent(
Fs,
Gs),
sequent(
cons(
p(
V),
Left),
Right)))
u'10'1(
reduce'ii'out) →
reduce'ii'outreduce'ii'in(
sequent(
Fs,
cons(
x'2b(
G1,
G2),
Gs)),
NF) →
u'11'1(
reduce'ii'in(
sequent(
Fs,
cons(
G1,
cons(
G2,
Gs))),
NF))
u'11'1(
reduce'ii'out) →
reduce'ii'outreduce'ii'in(
sequent(
Fs,
cons(
x'2a(
G1,
G2),
Gs)),
NF) →
u'12'1(
reduce'ii'in(
sequent(
Fs,
cons(
G1,
Gs)),
NF),
Fs,
G2,
Gs,
NF)
u'12'1(
reduce'ii'out,
Fs,
G2,
Gs,
NF) →
u'12'2(
reduce'ii'in(
sequent(
Fs,
cons(
G2,
Gs)),
NF))
u'12'2(
reduce'ii'out) →
reduce'ii'outreduce'ii'in(
sequent(
Fs,
cons(
x'2d(
G1),
Gs)),
NF) →
u'13'1(
reduce'ii'in(
sequent(
cons(
G1,
Fs),
Gs),
NF))
u'13'1(
reduce'ii'out) →
reduce'ii'outreduce'ii'in(
sequent(
nil,
cons(
p(
V),
Gs)),
sequent(
Left,
Right)) →
u'14'1(
reduce'ii'in(
sequent(
nil,
Gs),
sequent(
Left,
cons(
p(
V),
Right))))
u'14'1(
reduce'ii'out) →
reduce'ii'outreduce'ii'in(
sequent(
nil,
nil),
sequent(
F1,
F2)) →
u'15'1(
intersect'ii'in(
F1,
F2))
u'15'1(
intersect'ii'out) →
reduce'ii'outtautology'i'in(
F) →
u'16'1(
reduce'ii'in(
sequent(
nil,
cons(
F,
nil)),
sequent(
nil,
nil)))
u'16'1(
reduce'ii'out) →
tautology'i'outTypes:
intersect'ii'in :: cons:nil → cons:nil → intersect'ii'out
cons :: if:x'2d:x'2b:iff:x'2a:p → cons:nil → cons:nil
intersect'ii'out :: intersect'ii'out
u'1'1 :: intersect'ii'out → intersect'ii'out
u'2'1 :: intersect'ii'out → intersect'ii'out
reduce'ii'in :: sequent → sequent → reduce'ii'out
sequent :: cons:nil → cons:nil → sequent
if :: if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p
u'3'1 :: reduce'ii'out → reduce'ii'out
x'2b :: if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p
x'2d :: if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p
reduce'ii'out :: reduce'ii'out
iff :: if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p
u'4'1 :: reduce'ii'out → reduce'ii'out
x'2a :: if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p
u'5'1 :: reduce'ii'out → reduce'ii'out
u'6'1 :: reduce'ii'out → if:x'2d:x'2b:iff:x'2a:p → cons:nil → cons:nil → sequent → reduce'ii'out
u'6'2 :: reduce'ii'out → reduce'ii'out
u'7'1 :: reduce'ii'out → reduce'ii'out
u'8'1 :: reduce'ii'out → reduce'ii'out
u'9'1 :: reduce'ii'out → reduce'ii'out
p :: a → if:x'2d:x'2b:iff:x'2a:p
u'10'1 :: reduce'ii'out → reduce'ii'out
u'11'1 :: reduce'ii'out → reduce'ii'out
u'12'1 :: reduce'ii'out → cons:nil → if:x'2d:x'2b:iff:x'2a:p → cons:nil → sequent → reduce'ii'out
u'12'2 :: reduce'ii'out → reduce'ii'out
u'13'1 :: reduce'ii'out → reduce'ii'out
nil :: cons:nil
u'14'1 :: reduce'ii'out → reduce'ii'out
u'15'1 :: intersect'ii'out → reduce'ii'out
tautology'i'in :: if:x'2d:x'2b:iff:x'2a:p → tautology'i'out
u'16'1 :: reduce'ii'out → tautology'i'out
tautology'i'out :: tautology'i'out
hole_intersect'ii'out1_3 :: intersect'ii'out
hole_cons:nil2_3 :: cons:nil
hole_if:x'2d:x'2b:iff:x'2a:p3_3 :: if:x'2d:x'2b:iff:x'2a:p
hole_reduce'ii'out4_3 :: reduce'ii'out
hole_sequent5_3 :: sequent
hole_a6_3 :: a
hole_tautology'i'out7_3 :: tautology'i'out
gen_cons:nil8_3 :: Nat → cons:nil
gen_if:x'2d:x'2b:iff:x'2a:p9_3 :: Nat → if:x'2d:x'2b:iff:x'2a:p
Lemmas:
intersect'ii'in(gen_cons:nil8_3(a), gen_cons:nil8_3(+(1, n11_3))) → *10_3, rt ∈ Ω(n113)
Generator Equations:
gen_cons:nil8_3(0) ⇔ nil
gen_cons:nil8_3(+(x, 1)) ⇔ cons(p(hole_a6_3), gen_cons:nil8_3(x))
gen_if:x'2d:x'2b:iff:x'2a:p9_3(0) ⇔ p(hole_a6_3)
gen_if:x'2d:x'2b:iff:x'2a:p9_3(+(x, 1)) ⇔ if(p(hole_a6_3), gen_if:x'2d:x'2b:iff:x'2a:p9_3(x))
The following defined symbols remain to be analysed:
reduce'ii'in
(12) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol reduce'ii'in.
(13) Obligation:
TRS:
Rules:
intersect'ii'in(
cons(
X,
X0),
cons(
X,
X1)) →
intersect'ii'outintersect'ii'in(
Xs,
cons(
X0,
Ys)) →
u'1'1(
intersect'ii'in(
Xs,
Ys))
u'1'1(
intersect'ii'out) →
intersect'ii'outintersect'ii'in(
cons(
X0,
Xs),
Ys) →
u'2'1(
intersect'ii'in(
Xs,
Ys))
u'2'1(
intersect'ii'out) →
intersect'ii'outreduce'ii'in(
sequent(
cons(
if(
A,
B),
Fs),
Gs),
NF) →
u'3'1(
reduce'ii'in(
sequent(
cons(
x'2b(
x'2d(
B),
A),
Fs),
Gs),
NF))
u'3'1(
reduce'ii'out) →
reduce'ii'outreduce'ii'in(
sequent(
cons(
iff(
A,
B),
Fs),
Gs),
NF) →
u'4'1(
reduce'ii'in(
sequent(
cons(
x'2a(
if(
A,
B),
if(
B,
A)),
Fs),
Gs),
NF))
u'4'1(
reduce'ii'out) →
reduce'ii'outreduce'ii'in(
sequent(
cons(
x'2a(
F1,
F2),
Fs),
Gs),
NF) →
u'5'1(
reduce'ii'in(
sequent(
cons(
F1,
cons(
F2,
Fs)),
Gs),
NF))
u'5'1(
reduce'ii'out) →
reduce'ii'outreduce'ii'in(
sequent(
cons(
x'2b(
F1,
F2),
Fs),
Gs),
NF) →
u'6'1(
reduce'ii'in(
sequent(
cons(
F1,
Fs),
Gs),
NF),
F2,
Fs,
Gs,
NF)
u'6'1(
reduce'ii'out,
F2,
Fs,
Gs,
NF) →
u'6'2(
reduce'ii'in(
sequent(
cons(
F2,
Fs),
Gs),
NF))
u'6'2(
reduce'ii'out) →
reduce'ii'outreduce'ii'in(
sequent(
cons(
x'2d(
F1),
Fs),
Gs),
NF) →
u'7'1(
reduce'ii'in(
sequent(
Fs,
cons(
F1,
Gs)),
NF))
u'7'1(
reduce'ii'out) →
reduce'ii'outreduce'ii'in(
sequent(
Fs,
cons(
if(
A,
B),
Gs)),
NF) →
u'8'1(
reduce'ii'in(
sequent(
Fs,
cons(
x'2b(
x'2d(
B),
A),
Gs)),
NF))
u'8'1(
reduce'ii'out) →
reduce'ii'outreduce'ii'in(
sequent(
Fs,
cons(
iff(
A,
B),
Gs)),
NF) →
u'9'1(
reduce'ii'in(
sequent(
Fs,
cons(
x'2a(
if(
A,
B),
if(
B,
A)),
Gs)),
NF))
u'9'1(
reduce'ii'out) →
reduce'ii'outreduce'ii'in(
sequent(
cons(
p(
V),
Fs),
Gs),
sequent(
Left,
Right)) →
u'10'1(
reduce'ii'in(
sequent(
Fs,
Gs),
sequent(
cons(
p(
V),
Left),
Right)))
u'10'1(
reduce'ii'out) →
reduce'ii'outreduce'ii'in(
sequent(
Fs,
cons(
x'2b(
G1,
G2),
Gs)),
NF) →
u'11'1(
reduce'ii'in(
sequent(
Fs,
cons(
G1,
cons(
G2,
Gs))),
NF))
u'11'1(
reduce'ii'out) →
reduce'ii'outreduce'ii'in(
sequent(
Fs,
cons(
x'2a(
G1,
G2),
Gs)),
NF) →
u'12'1(
reduce'ii'in(
sequent(
Fs,
cons(
G1,
Gs)),
NF),
Fs,
G2,
Gs,
NF)
u'12'1(
reduce'ii'out,
Fs,
G2,
Gs,
NF) →
u'12'2(
reduce'ii'in(
sequent(
Fs,
cons(
G2,
Gs)),
NF))
u'12'2(
reduce'ii'out) →
reduce'ii'outreduce'ii'in(
sequent(
Fs,
cons(
x'2d(
G1),
Gs)),
NF) →
u'13'1(
reduce'ii'in(
sequent(
cons(
G1,
Fs),
Gs),
NF))
u'13'1(
reduce'ii'out) →
reduce'ii'outreduce'ii'in(
sequent(
nil,
cons(
p(
V),
Gs)),
sequent(
Left,
Right)) →
u'14'1(
reduce'ii'in(
sequent(
nil,
Gs),
sequent(
Left,
cons(
p(
V),
Right))))
u'14'1(
reduce'ii'out) →
reduce'ii'outreduce'ii'in(
sequent(
nil,
nil),
sequent(
F1,
F2)) →
u'15'1(
intersect'ii'in(
F1,
F2))
u'15'1(
intersect'ii'out) →
reduce'ii'outtautology'i'in(
F) →
u'16'1(
reduce'ii'in(
sequent(
nil,
cons(
F,
nil)),
sequent(
nil,
nil)))
u'16'1(
reduce'ii'out) →
tautology'i'outTypes:
intersect'ii'in :: cons:nil → cons:nil → intersect'ii'out
cons :: if:x'2d:x'2b:iff:x'2a:p → cons:nil → cons:nil
intersect'ii'out :: intersect'ii'out
u'1'1 :: intersect'ii'out → intersect'ii'out
u'2'1 :: intersect'ii'out → intersect'ii'out
reduce'ii'in :: sequent → sequent → reduce'ii'out
sequent :: cons:nil → cons:nil → sequent
if :: if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p
u'3'1 :: reduce'ii'out → reduce'ii'out
x'2b :: if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p
x'2d :: if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p
reduce'ii'out :: reduce'ii'out
iff :: if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p
u'4'1 :: reduce'ii'out → reduce'ii'out
x'2a :: if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p
u'5'1 :: reduce'ii'out → reduce'ii'out
u'6'1 :: reduce'ii'out → if:x'2d:x'2b:iff:x'2a:p → cons:nil → cons:nil → sequent → reduce'ii'out
u'6'2 :: reduce'ii'out → reduce'ii'out
u'7'1 :: reduce'ii'out → reduce'ii'out
u'8'1 :: reduce'ii'out → reduce'ii'out
u'9'1 :: reduce'ii'out → reduce'ii'out
p :: a → if:x'2d:x'2b:iff:x'2a:p
u'10'1 :: reduce'ii'out → reduce'ii'out
u'11'1 :: reduce'ii'out → reduce'ii'out
u'12'1 :: reduce'ii'out → cons:nil → if:x'2d:x'2b:iff:x'2a:p → cons:nil → sequent → reduce'ii'out
u'12'2 :: reduce'ii'out → reduce'ii'out
u'13'1 :: reduce'ii'out → reduce'ii'out
nil :: cons:nil
u'14'1 :: reduce'ii'out → reduce'ii'out
u'15'1 :: intersect'ii'out → reduce'ii'out
tautology'i'in :: if:x'2d:x'2b:iff:x'2a:p → tautology'i'out
u'16'1 :: reduce'ii'out → tautology'i'out
tautology'i'out :: tautology'i'out
hole_intersect'ii'out1_3 :: intersect'ii'out
hole_cons:nil2_3 :: cons:nil
hole_if:x'2d:x'2b:iff:x'2a:p3_3 :: if:x'2d:x'2b:iff:x'2a:p
hole_reduce'ii'out4_3 :: reduce'ii'out
hole_sequent5_3 :: sequent
hole_a6_3 :: a
hole_tautology'i'out7_3 :: tautology'i'out
gen_cons:nil8_3 :: Nat → cons:nil
gen_if:x'2d:x'2b:iff:x'2a:p9_3 :: Nat → if:x'2d:x'2b:iff:x'2a:p
Lemmas:
intersect'ii'in(gen_cons:nil8_3(a), gen_cons:nil8_3(+(1, n11_3))) → *10_3, rt ∈ Ω(n113)
Generator Equations:
gen_cons:nil8_3(0) ⇔ nil
gen_cons:nil8_3(+(x, 1)) ⇔ cons(p(hole_a6_3), gen_cons:nil8_3(x))
gen_if:x'2d:x'2b:iff:x'2a:p9_3(0) ⇔ p(hole_a6_3)
gen_if:x'2d:x'2b:iff:x'2a:p9_3(+(x, 1)) ⇔ if(p(hole_a6_3), gen_if:x'2d:x'2b:iff:x'2a:p9_3(x))
No more defined symbols left to analyse.
(14) LowerBoundsProof (EQUIVALENT transformation)
The lowerbound Ω(n1) was proven with the following lemma:
intersect'ii'in(gen_cons:nil8_3(a), gen_cons:nil8_3(+(1, n11_3))) → *10_3, rt ∈ Ω(n113)
(15) BOUNDS(n^1, INF)
(16) Obligation:
TRS:
Rules:
intersect'ii'in(
cons(
X,
X0),
cons(
X,
X1)) →
intersect'ii'outintersect'ii'in(
Xs,
cons(
X0,
Ys)) →
u'1'1(
intersect'ii'in(
Xs,
Ys))
u'1'1(
intersect'ii'out) →
intersect'ii'outintersect'ii'in(
cons(
X0,
Xs),
Ys) →
u'2'1(
intersect'ii'in(
Xs,
Ys))
u'2'1(
intersect'ii'out) →
intersect'ii'outreduce'ii'in(
sequent(
cons(
if(
A,
B),
Fs),
Gs),
NF) →
u'3'1(
reduce'ii'in(
sequent(
cons(
x'2b(
x'2d(
B),
A),
Fs),
Gs),
NF))
u'3'1(
reduce'ii'out) →
reduce'ii'outreduce'ii'in(
sequent(
cons(
iff(
A,
B),
Fs),
Gs),
NF) →
u'4'1(
reduce'ii'in(
sequent(
cons(
x'2a(
if(
A,
B),
if(
B,
A)),
Fs),
Gs),
NF))
u'4'1(
reduce'ii'out) →
reduce'ii'outreduce'ii'in(
sequent(
cons(
x'2a(
F1,
F2),
Fs),
Gs),
NF) →
u'5'1(
reduce'ii'in(
sequent(
cons(
F1,
cons(
F2,
Fs)),
Gs),
NF))
u'5'1(
reduce'ii'out) →
reduce'ii'outreduce'ii'in(
sequent(
cons(
x'2b(
F1,
F2),
Fs),
Gs),
NF) →
u'6'1(
reduce'ii'in(
sequent(
cons(
F1,
Fs),
Gs),
NF),
F2,
Fs,
Gs,
NF)
u'6'1(
reduce'ii'out,
F2,
Fs,
Gs,
NF) →
u'6'2(
reduce'ii'in(
sequent(
cons(
F2,
Fs),
Gs),
NF))
u'6'2(
reduce'ii'out) →
reduce'ii'outreduce'ii'in(
sequent(
cons(
x'2d(
F1),
Fs),
Gs),
NF) →
u'7'1(
reduce'ii'in(
sequent(
Fs,
cons(
F1,
Gs)),
NF))
u'7'1(
reduce'ii'out) →
reduce'ii'outreduce'ii'in(
sequent(
Fs,
cons(
if(
A,
B),
Gs)),
NF) →
u'8'1(
reduce'ii'in(
sequent(
Fs,
cons(
x'2b(
x'2d(
B),
A),
Gs)),
NF))
u'8'1(
reduce'ii'out) →
reduce'ii'outreduce'ii'in(
sequent(
Fs,
cons(
iff(
A,
B),
Gs)),
NF) →
u'9'1(
reduce'ii'in(
sequent(
Fs,
cons(
x'2a(
if(
A,
B),
if(
B,
A)),
Gs)),
NF))
u'9'1(
reduce'ii'out) →
reduce'ii'outreduce'ii'in(
sequent(
cons(
p(
V),
Fs),
Gs),
sequent(
Left,
Right)) →
u'10'1(
reduce'ii'in(
sequent(
Fs,
Gs),
sequent(
cons(
p(
V),
Left),
Right)))
u'10'1(
reduce'ii'out) →
reduce'ii'outreduce'ii'in(
sequent(
Fs,
cons(
x'2b(
G1,
G2),
Gs)),
NF) →
u'11'1(
reduce'ii'in(
sequent(
Fs,
cons(
G1,
cons(
G2,
Gs))),
NF))
u'11'1(
reduce'ii'out) →
reduce'ii'outreduce'ii'in(
sequent(
Fs,
cons(
x'2a(
G1,
G2),
Gs)),
NF) →
u'12'1(
reduce'ii'in(
sequent(
Fs,
cons(
G1,
Gs)),
NF),
Fs,
G2,
Gs,
NF)
u'12'1(
reduce'ii'out,
Fs,
G2,
Gs,
NF) →
u'12'2(
reduce'ii'in(
sequent(
Fs,
cons(
G2,
Gs)),
NF))
u'12'2(
reduce'ii'out) →
reduce'ii'outreduce'ii'in(
sequent(
Fs,
cons(
x'2d(
G1),
Gs)),
NF) →
u'13'1(
reduce'ii'in(
sequent(
cons(
G1,
Fs),
Gs),
NF))
u'13'1(
reduce'ii'out) →
reduce'ii'outreduce'ii'in(
sequent(
nil,
cons(
p(
V),
Gs)),
sequent(
Left,
Right)) →
u'14'1(
reduce'ii'in(
sequent(
nil,
Gs),
sequent(
Left,
cons(
p(
V),
Right))))
u'14'1(
reduce'ii'out) →
reduce'ii'outreduce'ii'in(
sequent(
nil,
nil),
sequent(
F1,
F2)) →
u'15'1(
intersect'ii'in(
F1,
F2))
u'15'1(
intersect'ii'out) →
reduce'ii'outtautology'i'in(
F) →
u'16'1(
reduce'ii'in(
sequent(
nil,
cons(
F,
nil)),
sequent(
nil,
nil)))
u'16'1(
reduce'ii'out) →
tautology'i'outTypes:
intersect'ii'in :: cons:nil → cons:nil → intersect'ii'out
cons :: if:x'2d:x'2b:iff:x'2a:p → cons:nil → cons:nil
intersect'ii'out :: intersect'ii'out
u'1'1 :: intersect'ii'out → intersect'ii'out
u'2'1 :: intersect'ii'out → intersect'ii'out
reduce'ii'in :: sequent → sequent → reduce'ii'out
sequent :: cons:nil → cons:nil → sequent
if :: if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p
u'3'1 :: reduce'ii'out → reduce'ii'out
x'2b :: if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p
x'2d :: if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p
reduce'ii'out :: reduce'ii'out
iff :: if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p
u'4'1 :: reduce'ii'out → reduce'ii'out
x'2a :: if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p → if:x'2d:x'2b:iff:x'2a:p
u'5'1 :: reduce'ii'out → reduce'ii'out
u'6'1 :: reduce'ii'out → if:x'2d:x'2b:iff:x'2a:p → cons:nil → cons:nil → sequent → reduce'ii'out
u'6'2 :: reduce'ii'out → reduce'ii'out
u'7'1 :: reduce'ii'out → reduce'ii'out
u'8'1 :: reduce'ii'out → reduce'ii'out
u'9'1 :: reduce'ii'out → reduce'ii'out
p :: a → if:x'2d:x'2b:iff:x'2a:p
u'10'1 :: reduce'ii'out → reduce'ii'out
u'11'1 :: reduce'ii'out → reduce'ii'out
u'12'1 :: reduce'ii'out → cons:nil → if:x'2d:x'2b:iff:x'2a:p → cons:nil → sequent → reduce'ii'out
u'12'2 :: reduce'ii'out → reduce'ii'out
u'13'1 :: reduce'ii'out → reduce'ii'out
nil :: cons:nil
u'14'1 :: reduce'ii'out → reduce'ii'out
u'15'1 :: intersect'ii'out → reduce'ii'out
tautology'i'in :: if:x'2d:x'2b:iff:x'2a:p → tautology'i'out
u'16'1 :: reduce'ii'out → tautology'i'out
tautology'i'out :: tautology'i'out
hole_intersect'ii'out1_3 :: intersect'ii'out
hole_cons:nil2_3 :: cons:nil
hole_if:x'2d:x'2b:iff:x'2a:p3_3 :: if:x'2d:x'2b:iff:x'2a:p
hole_reduce'ii'out4_3 :: reduce'ii'out
hole_sequent5_3 :: sequent
hole_a6_3 :: a
hole_tautology'i'out7_3 :: tautology'i'out
gen_cons:nil8_3 :: Nat → cons:nil
gen_if:x'2d:x'2b:iff:x'2a:p9_3 :: Nat → if:x'2d:x'2b:iff:x'2a:p
Lemmas:
intersect'ii'in(gen_cons:nil8_3(a), gen_cons:nil8_3(+(1, n11_3))) → *10_3, rt ∈ Ω(n113)
Generator Equations:
gen_cons:nil8_3(0) ⇔ nil
gen_cons:nil8_3(+(x, 1)) ⇔ cons(p(hole_a6_3), gen_cons:nil8_3(x))
gen_if:x'2d:x'2b:iff:x'2a:p9_3(0) ⇔ p(hole_a6_3)
gen_if:x'2d:x'2b:iff:x'2a:p9_3(+(x, 1)) ⇔ if(p(hole_a6_3), gen_if:x'2d:x'2b:iff:x'2a:p9_3(x))
No more defined symbols left to analyse.
(17) LowerBoundsProof (EQUIVALENT transformation)
The lowerbound Ω(n1) was proven with the following lemma:
intersect'ii'in(gen_cons:nil8_3(a), gen_cons:nil8_3(+(1, n11_3))) → *10_3, rt ∈ Ω(n113)
(18) BOUNDS(n^1, INF)